$\forall$$B$:Type, $P$:($B$$\rightarrow$Prop). $\Box$!$P$ $\in$ ($B$$\rightarrow$Type)$\rightarrow$Prop